Nuprl Lemma : loset_connex
13,42
postcript
pdf
s
:LOSet,
x
,
y
:|
s
|. (
x
y
)
(
y
x
)
latex
Up
sets
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Connex(
T
;
x
,
y
.
R
(
x
;
y
))
Lemmas
loset
wf
,
loset
properties
origin
s:LOSet, x, y:|s|. (x 
y) 
(y x) s:LOSet, x, y:|s|. (x y) (y x) 
Tx:A. B(x)